\begin{tabbing}
es{-}first{-}at{-}since(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}loc(${\it es}$; $e$) $=$ $i$ $\in$ Id\+
\\[0ex]\& $P$($e$) \& $\neg$$R$($e$)
\\[0ex]\& alle{-}lt(${\it es}$;$e$;${\it e'}$.\=$P$(${\it e'}$)\+
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e''}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}le(${\it es}$;${\it e'}$;${\it e''}$) \& es{-}locl(${\it es}$; ${\it e''}$; $e$) \& $R$(${\it e''}$)))
\-\-\-
\end{tabbing}